/**
 *  TiniSatJ :: A Java implemented SAT Solver based on Tinisat 0.22
 *
 *  Copyright (C) 2007 KITAGAWA, Satoshi.
 *
 *  Original TiniSat is available from
 *  http://users.rsise.anu.edu.au/~jinbo/tinisat/
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 */

package com.googlecode.tinisat_j;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.Vector;
import java.util.Map.Entry;

import org.apache.commons.collections.primitives.ArrayIntList;
import org.apache.commons.collections.primitives.IntListIterator;

public class CnfManager {

    protected int vc;
    protected Var[] vars;

    protected int[] varOrder;
    protected int[] varPosition;
    protected int nextVar;

    protected Vector<int[]> clauses;
    protected int nextClause;

    protected int[] stack;
    protected int stackTop;
    protected LinkedList<int[]> litPools;

    protected int aLevel;
    protected int dLevel;
    protected int nDecisions;
    protected int nConflicts;
    protected int nRestarts;
    protected ArrayIntList conflictLits;
    protected ArrayIntList tmpConflictLits;
    protected int[] conflictClause;

    protected boolean FREE(int lit) { return (vars[Var.VAR(lit)].value == Var.FREE); }
    protected boolean SET(int lit) { return (vars[Var.VAR(lit)].value == Var.SIGN(lit)); }
    protected boolean RESOLVED(int lit) { return (vars[Var.VAR(lit)].value == Var.SIGN(Var.NEG(lit))); }
    protected Vector<int[]> WATCHLIST(int lit) { return (vars[Var.VAR(lit)].watch[Var.SIGN(lit)]); }
    protected int[] IMPLIST(int lit) { return vars[Var.VAR(lit)].imp[Var.SIGN(lit)]; };
    protected int SCORE(int var) { return vars[var].score(); }


    @SuppressWarnings("unchecked")
    protected CnfManager(Cnf cnf) {
        vars = new Var[ (vc = cnf.vc) + 1];
        for (int i=0; i<vars.length; i++) {
            vars[i] = new Var(i);
        }
        clauses = new Vector<int[]>();
        dLevel = 1;
        nDecisions = nConflicts = nRestarts = 0;

        stack = new int[vc+1];
        stackTop = 0;

        HashMap<Integer, ArrayIntList> imp[] = new HashMap[] {
                new HashMap<Integer, ArrayIntList>(vc+1),
                new HashMap<Integer, ArrayIntList>(vc+1)
        };

        varOrder = new int[vc+1];
        varPosition = new int[vc+1];

        // mark bottom of stack with variable 0
        stack[stackTop++] = 0;
        vars[0].dLevel = 0;
        vars[0].value = Var.FREE;


        litPools = new LinkedList<int[]> ();
        conflictLits = new ArrayIntList();
        tmpConflictLits = new ArrayIntList();


        //populate litPool
        for (int i=0; i < cnf.cc; i++) {
            int[] lits = cnf.clauses[i]; // current clause
            if (lits[1] == 0) { // unit clause
                int lit = lits[0];
                if (FREE(lit)) {
                    stack[stackTop++] = lit;
                    setLiteral(lit, stack);
                }
                else if (RESOLVED(lit)) {
                    System.out.print("c contradictory unit claused " +  (lit) + ", " + (-lit) + "\n");
                    System.out.print("s UNSATISFIABLE\n");
                    System.exit(20);
                }
            }
            else if (lits[2] == 0) { // binary clause
                int lit0 = lits[0];
                int var0 = Var.VAR(lit0);
                int lit1 = lits[1];
                int var1 = Var.VAR(lit1);
                ArrayIntList deq;
                if ( (deq = imp[Var.SIGN(lit0)].get(var0)) == null ) {
                    deq = new ArrayIntList();
                    imp[Var.SIGN(lit0)].put(var0, deq);
                }
                deq.add(lit1);

                if ( (deq = imp[Var.SIGN(lit1)].get(var1)) == null ) {
                    deq = new ArrayIntList();
                    imp[Var.SIGN(lit1)].put(var1, deq);
                }
                deq.add(lit0);
                vars[var0].activity[Var.SIGN(lit0)]++;
                vars[var1].activity[Var.SIGN(lit1)]++;
            }
            else {
            	int[] clause = new int[lits.length];
                litPools.add(clause);
                // set up watches

                int lit = lits[0];
                Vector<int[]> wl = WATCHLIST(lit);
                wl.add(clause);

                lit = lits[1];
                wl = WATCHLIST(lit);
                wl.add(clause);

                // copy literals to litPool
                for (int j=0; (lit = lits[j]) != 0; j++) {
                	clause[j] = lits[j];
                    vars[Var.VAR(lit)].activity[Var.SIGN(lit)]++;
                }
            }
        }

        // binary clause implication lists
        // last element is 0
        // first three elements are ([], lit, 0)
        // serve as antecedent for all implications
        // serve as conflicting clause with [] filled
        for(int i = 0; i <= 1; i++){
            for (Entry<Integer, ArrayIntList> entry : imp[i].entrySet()) {
                int val = entry.getKey();
                ArrayIntList deq = entry.getValue();
                int[] imp_ = new int[deq.size() + 4];
                vars[val].imp[i] = imp_;
                imp_[1] = val * ((i == Var.POSI) ? 1 : -1);
                int k = 3;
                IntListIterator itr = deq.listIterator();
                while (itr.hasNext()) {
                    imp_[k++] = itr.next();
                }
                imp_[k] = 0;
            }
        }

        // assert unit clauses
        assertUnitClauses();

    }

    protected boolean assertUnitClauses() {

        for (int p = (stackTop - 1); stack[p] != 0; p--) {
            int lit = stack[p];
            stack[p] = stack[(--stackTop)];
            if (!assertLiteral(lit, null)) {
                backtrack(dLevel - 1);
                return false;
            }
        }
        return true;
    }

    protected void setLiteral(int lit, int[] ante) {
        Var tmp_var = vars[Var.VAR(lit)];
        tmp_var.value = Var.SIGN(lit);
        tmp_var.ante = ante;
        tmp_var.dLevel = dLevel;
    }

    protected boolean assertLiteral(int lit, int[] ante) {
    	int stackDiff = -stackTop;
        int newStackTop = stackTop;
        stack[newStackTop++] = lit;
        setLiteral(lit, ante);

        while(stackTop < newStackTop) {
            int nlit = Var.NEG(stack[stackTop++]);

            // implications via binary clauses
            int[] impList = IMPLIST(nlit);
            for(int i = 3; impList != null; i++){
                // implication
                if(FREE(impList[i])){
                    if(impList[i] == 0) break;   // end of list

                    setLiteral(stack[newStackTop++] = impList[i], impList);
                    //     contradiction
                }else if(RESOLVED(impList[i])){
                    nConflicts++;
                    stackTop = newStackTop;
                    // make up temporary binary clause
                    impList[0] = impList[i];
                    learnClause(impList);  // for clause learning purposes
                    return false;
                }
            }

            // other implications
            Vector<int[]> watchList = WATCHLIST(nlit);

            for (int i=0; i < watchList.size(); i++) {
                int[] clause = watchList.get(i);
                int first, watch, otherWatch;
                first = 0;
                if (clause[first] == nlit) { watch = 0; otherWatch = 1; }
                else { watch = 1; otherWatch = 0; };

                if (SET(clause[otherWatch])) continue;

                int p = 2;
                boolean found = true;
                while (RESOLVED(clause[p])) {
                    assert (clause[p] == 0) : vars[Var.VAR(clause[p])].value;
                    p++;
                }

                if (clause[p] == 0) found = false;

                if (found) {
                    WATCHLIST(clause[p]).add(clause);
                    int last_index = watchList.size() - 1;
                    int[] last = watchList.get(last_index);
                    watchList.setElementAt(last, i--);
                    watchList.remove(watchList.size() -1);

                    int x = clause[watch];
                    clause[watch] = clause[p];
                    clause[p] = x;
                }
                else {
                    if (FREE(clause[otherWatch])) {
                        stack[newStackTop++] = clause[otherWatch];
                        setLiteral(clause[otherWatch], clause);

                        if (otherWatch != first) {
                            int x = clause[otherWatch];
                            clause[otherWatch] = clause[first];
                            clause[first] = x;
                        }
                    }
                    else if (RESOLVED(clause[otherWatch])){
                        nConflicts++;
                        stackTop = newStackTop;
                        learnClause(clause);
                        return false;
                    }
                }
            }
        }
        stackDiff += stackTop;
        vars[Var.VAR(lit)].activity[Var.SIGN(lit)] += stackDiff;
        return true;
    }

    protected void learnClause(int[]  clause) {
        if (dLevel == 1) { aLevel = 0; return; };

        updateScores(clause);

        conflictLits.clear();
        int curLevelLits = 0;

        tmpConflictLits.clear();
        int lit;
        for (int i=0; (lit = clause[i]) != 0; i++) {
            Var var = vars[Var.VAR(lit)];
            if (var.dLevel == 1) continue;

            if (var.dLevel < dLevel) tmpConflictLits.add(lit);
            else curLevelLits++;

            var.mark = true;
        }

        while (true) {
            lit = stack[--stackTop];
            int var_Id = Var.VAR(lit);
            Var var = vars[var_Id];
            var.value = Var.FREE;
            int varPos = varPosition[var_Id];
            if (!var.mark) {
                if (varPos < nextVar) nextVar = varPos;
                continue;
            }

            var.mark = false;
            int[] ante = var.ante;
            var.ante = null;
            if (ante != null) updateScores(ante);

            // varPosition may change in updateScores()
            varPos = varPosition[var_Id];
            if (varPos < nextVar) nextVar = varPos;

            if (curLevelLits-- == 1) break;

            int alit = 0;
            for (int i=1; ante != null && (alit = ante[i]) != 0; i++) {
            	Var v = vars[Var.VAR(alit)];
                if (v.mark || v.dLevel == 1) continue;
                if (v.dLevel < dLevel) tmpConflictLits.add(alit);
                else curLevelLits++;
                v.mark = true;
            }
        }

        aLevel = 1;
        IntListIterator cLits = tmpConflictLits.listIterator();

        while (cLits.hasNext()) {
            boolean redundant = true;
            int clit = cLits.next();
            int[] ante = vars[Var.VAR(clit)].ante;
            if (ante == null) redundant = false;
            else {
                int alit;
                for (int i=1; (alit = ante[i]) != 0; i++) {
                    if (!vars[Var.VAR(alit)].mark) {
                        redundant = false;
                        break;
                    }
                }
            }
            if (!redundant) {
                if (vars[Var.VAR(clit)].dLevel > aLevel) {
                    aLevel = vars[Var.VAR(clit)].dLevel;
                    conflictLits.add(0, clit);
                }
                else conflictLits.add(clit);
            }
        }

        cLits = tmpConflictLits.listIterator();
        while (cLits.hasNext()) {
            vars[Var.VAR(cLits.next())].mark = false;
        }

        conflictLits.add(-lit);

        addClause();
    }

    protected void addClause() {
        int size = conflictLits.size();
        conflictClause = new int[size+2];
        conflictClause[0] = conflictLits.get(size - 1);

        if (size > 1) {

            conflictClause[1] = conflictLits.get(0);

            WATCHLIST(conflictClause[0]).add(conflictClause);
            WATCHLIST(conflictClause[1]).add(conflictClause);

        }
        for (int i=1; i<size-1; i++) {
            conflictClause[i+1] = conflictLits.get(i);
        }

        conflictClause[size] = 0;
        litPools.add(conflictClause);
        conflictLits.clear();
    }

    protected void updateScores(int[] p) {

        int lit;
        for (int i=0; (lit = p[i]) != 0; i++) {

            int v = Var.VAR(lit);
            Var var = vars[v];
            var.activity[Var.SIGN(lit)]++;


            int it = varPosition[v];
            if (it == 0) continue;

            int score = var.score();


            if (score <= SCORE(varOrder[it-1])) continue;

            int step = 0x400, q;

            for (q = it - step; q >= 0; q -= step)
                if (SCORE(varOrder[q]) >= score) break;
            for (q += step, step >>= 1; step >0; step >>=1) {
                if (q - step >= 0)
                    if (SCORE(varOrder[q - step]) < score)
                        q -= step;
            }

            // swap it and q
            varOrder[it] = varOrder[q];
            varPosition[v] = q;
            varPosition[varOrder[q]] = it;
            varOrder[q] = v;

        }
    }


    protected boolean assertCL() {
        if (conflictClause != null) {
            return assertLiteral(conflictClause[0], conflictClause);
        }
        return false;
    }

    protected boolean decide(int lit) {
        nDecisions++; dLevel++;
        return assertLiteral(lit, null);
    }

    protected void backtrack(int bLevel) {
        int var_Id;
        while ( vars[var_Id = Var.VAR(stack[stackTop-1])].dLevel > bLevel) {
            Var var = vars[var_Id];
            if (var.dLevel < dLevel) var.phase = var.value;
            var.value = Var.FREE;
            int varPos = varOrder[var_Id];
            if (varPos < nextVar) nextVar = varPos;
            stackTop--;
        }
        dLevel = bLevel;
    }

    protected void scoreDecay() {
        for (int i=1; i <= vc; i++) {
            vars[i].activity[0] >>= 1;
            vars[i].activity[1] >>= 1;
        }
    }
}
